i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(k:{k:Knd| 
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(k:{(k  ks)} 
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(decl-state(ds)
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(ma-valtype(da; k)
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(TT).
fpf-compatible(Id; x.Type; id-deq; ds; fpf-single(x; T))
 (k:Knd. 
 (fpf-dom(Kind-deq; k; R-da(R-state-var(i; ds; da; x; T; ks; tr); i)))  (k  ks)) 

latex

Definitions

False, P  Q, A, void, t  T, isect(A; x.B(x)), top, x. t(x), x:A. B(x), x:AB(x), fpf-dom(eq; x; f), b, (x  l), Id, prop{i:l}, b, , x:A  B(x), P  Q, P  Q, Unit, left + right, <a, b>, type List, decl-state(ds), {x:A| B(x)} , id-deq, fpf-compatible(A; a.B(a); eq; f; g), fpf-empty, ma-valtype(da; k), fpf-single(x; v), Kind-deq, fpf-join(eq; f; g), x.A(x), reduce(f; k; as), eq_id(a; b), if b then t else f fi , R-state-var(i; ds; da; x; T; ks; tr), R-da(R; i), Type, Knd, fpf(A; a.B(a)), s = t, guard(T), P  Q, P  Q

Lemmas

false wf, fpf-join-dom-sq, assert of bor, cons member, fpf-single-dom, R-da wf, R-state-var wf, fpf-compatible wf, id-deq wf, decl-state wf, l member wf, fpf-trivial-subtype-top, R-state-var-da, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, bnot wf, not wf, Id wf, assert wf, fpf-dom wf, reduce wf, fpf-join wf, fpf-single wf, ma-valtype wf, Kind-deq wf, fpf wf, fpf-empty wf, top wf, Knd wf